Nuprl Lemma : equal-top
0,22
postcript
pdf
x
,
y
:Top.
x
=
y
latex
Definitions
Void
,
t
T
,
x
:
A
.
B
(
x
)
,
s
=
t
,
x
:
A
.
B
(
x
)
,
Top
origin
x, y:Top. x = y x, y:Top. x = y 
T
x:A. B(x)x:A. B(x)